-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x
↳ QTRS
↳ DependencyPairsProof
-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x
-1(x, s(y)) → P(s(y))
-1(x, s(y)) → -1(x, p(s(y)))
-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
-1(x, s(y)) → P(s(y))
-1(x, s(y)) → -1(x, p(s(y)))
-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
-1(x, s(y)) → -1(x, p(s(y)))
-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-1(x, s(y)) → -1(x, p(s(y)))
The value of delta used in the strict ordering is 9/16.
POL(-1(x1, x2)) = (9/4)x_2
POL(s(x1)) = 1/2 + (9/4)x_1
POL(p(x1)) = (1/2)x_1
p(s(x)) → x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
-(0, y) → 0
-(x, 0) → x
-(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0)
p(0) → 0
p(s(x)) → x